$\forall$$A$, $B_{0}$, $B_{1}$, $C$:Type, $f$:($A$$\rightarrow$$B_{0}$), $g$:($B_{1}$$\rightarrow$$C$).
\\[0ex]strong{-}subtype($B_{0}$;$B_{1}$) $\Rightarrow$ Inj($A$;$B_{0}$;$f$) $\Rightarrow$ Inj($B_{1}$;$C$;$g$) $\Rightarrow$ Inj($A$;$C$;$g$ o $f$)